Governance: TLA Codelink for refresh_neuron #3547
Conversation
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
If this pull request affects the behavior of any canister owned by
the Governance team, remember to update the corresponding
unreleased_changes.md file(s).
To acknowldge this reminder (and unblock the PR), dismiss this
code review by going to the bottom of the pull request page, and
supply one of the following reasons:
-
Done.
-
No canister behavior changes.
andrew-lee-work
dismissed
github-actions[bot]’s stale review
No canister behavior changes.
| @@ -6325,6 +6327,7 @@ impl Governance { | |||
| )?; | |||
|
|
|||
| // Get the balance of the neuron from the ledger canister. | |||
| tla_log_locals! { account: tla::account_to_tla(account), neuron_id: nid.id }; | |||
There was a problem hiding this comment.
Do you need the account here (and in the model)? AFAICT you can derive it from the global state (neuron in the model).
| OP_ACCOUNT_BALANCE == "account_balance" | ||
| ACCOUNT_BALANCE_FAIL == "Err" |
There was a problem hiding this comment.
These seem unused? And if you get rid of the account local variable I think you can also get rid of DUMMY_ACCOUNT.
| if(answer.response /= Variant("Fail", UNIT)) { | ||
| with (b = VariantGetOrElse("BalanceQueryOk", answer.response, 0)) { | ||
| if(b >= MIN_STAKE) { | ||
| neuron := [neuron EXCEPT ![neuron_id] = [@ EXCEPT !.cached_stake = b] ] |
There was a problem hiding this comment.
Apparently you can also write
| neuron := [neuron EXCEPT ![neuron_id] = [@ EXCEPT !.cached_stake = b] ] | |
| neuron := [neuron EXCEPT ![neuron_id].cached_stake = b ] |
(I wasn't aware of this syntax before).
Also, I'm thinking that we may want to have an invariant that the cached stake of a neuron subaccount doesn't go below min stake... Though I'm not sure if this always holds or we'd need some side conditions on it (for example, if the user deposits less than MIN_STAKE and tries to create a neuron, maybe it's temporarily violated)
Instrument refresh_neuron and its tests for TLA Code Link, add TLA model for refresh neuron.